T:Type, L1, L2:T List, P, Q:(T).
(L1 agree_on(T;a.P(a)) L2)
 index-of-first a in L1.P(a)  Q(a) = index-of-first a in L2.P(a)  Q(a)   

latex

Definitions	x:A. B(x), ij, ||as||, index-of-first x in L.P(x), t  T, x. t(x), , x(s), p  q, A & B, P  Q, False, A, P & Q, AB, i  j < k, {i..j}, P  Q, l[i], b, Prop, , x f y, agree_on(T;x.P(x)), if b t else f fi, {T}, SQType(T), True, P  Q, T, P  Q, Dec(P), hd(l), i<j, ij, b, Unit
Lemmas	false wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, lt int wf, ifthenelse wf, decidable or, decidable assert, squash wf, true wf, select cons tl, first index cons, length wf2, bool wf, length wf1, int seg wf, assert wf, select wf, non neg length, band wf, nat wf, first index wf